$\forall$${\it the\_es}$:event\_system\{i:l\}. SWellFounded(es{-}locl(${\it the\_es}$; $x$; $y$))